1. $i$ : $\mathbb{N}$
\\[0ex]2. $f$ : \{$f$ $\mid$ $i$:\{$z$:$\mathbb{N}\mid$ $z$ $<$ $i$\}  $\rightarrow$ if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi \}
\\[0ex]3. $j$ : $\mathbb{N}$
\\[0ex]4. $\forall$$j_{1}$:$\mathbb{N}$. ($j_{1}$ $<$ $j$) $\Rightarrow$ ($j_{1}$ $<$ $i$) $\Rightarrow$ ($f$($j_{1}$) $\in$ $\mathbb{Z}$)
\\[0ex]$\vdash$  ($j$ $<$ $i$) $\Rightarrow$ ($f$($j$) $\in$ $\mathbb{Z}$)